Raonament automatitzat

En informàtica, en particular en la representació del coneixement i el raonament i la metalògica, l'àrea del raonament automatitzat es dedica a comprendre diferents aspectes del raonament. L'estudi del raonament automatitzat ajuda a produir programes informàtics que permeten als ordinadors raonar completament, o gairebé completament, automàticament. Tot i que el raonament automatitzat es considera un subcamp de la intel·ligència artificial, també té connexions amb la informàtica teòrica i la filosofia.^[1]

Les subàrees més desenvolupades del raonament automatitzat són la demostració automatitzada de teoremes (i el subcamp menys automatitzat però més pragmàtic de la demostració interactiva de teoremes) i la verificació de proves automatitzada (vist com un raonament correcte garantit sota supòsits fixos). També s'ha fet un treball extens en el raonament per analogia utilitzant inducció i abducció.^[1]

Altres temes importants inclouen el raonament sota incertesa i el raonament no monòton. Una part important del camp d'incertesa és el de l'argumentació, on s'apliquen més restriccions de minimalitat i consistència a la deducció automatitzada més estàndard. El sistema OSCAR de John Pollock és un exemple de sistema d'argumentació automatitzat que és més específic que només un demostrador de teoremes automatitzat.^[2]

Les eines i tècniques de raonament automatitzat inclouen la lògica clàssica i els càlculs, la lògica difusa, la inferència bayesiana, el raonament amb entropia màxima i moltes tècniques ad hoc menys formals.